First evaluations of expr conversions on the bench/coreutils folder revealed the following conversion success/failure stats:

cp:

76.63% Good
 4.15% Overflow
 3.64% Lval: Mem.Accessor
 3.17% LNot
 3.09% Lval: Mem
 2.55% NonIntConst
 2.01% BinOp_not_supported
 1.75% Ask_yields_bot
 0.91% Lval: Var.Accessor
 0.84% CastE
 0.42% other
 0.35% Cast_not_injective
 0.22% Invalid_argument
 0.20% SizeOfXXX

cksum:

52.23% Success
16.52% Lval: Mem.Accessor
11.31% Lval: Mem
 8.27% Ask_yields_bot
 4.81% LNot
 2.70% Overflow
 1.50% NonIntConst
 1.09% BinOp_not_supported
 0.52% Cast_not_injective
 0.48% other
 0.45% CastE
 0.11% Lval: Var.Accessor

Overall, my worries, that overflow-treatment and non-injective assignments would stop the show seem not to be the major issue in these examples. I am curious how far we can push the success rate. A few first steps:

• Ask_yields_bot demands thinking about how to handle pointers in evalInt queries, which has been ignored in the conversion so far
• shifts are not implemented at all right now
• can we do something about ternary operators?
• Logical Not might be worthwhile to pursue at least partially e.g. when occuring top-level

More long-term thoughts:

• The unsupported Lvals like pointer, struct and arrays might need some concept of how to deal with them
• Mapping Array index arithmetics into the linear expression would maybe yield a few more noteworthy invariants

After replacing the raised exception in the conversion's queryInt with a returned top, we could immediately gain roughly 10 points success percentage for both cases, eg. for cksum:

62.2487% Good
16.8537% Exp_not_supported:LValMem.FieldAccessor
 9.65872% Exp_not_supported:LValMem
 4.76858% Exp_not_supported:LValVar(untracked):
 2.78635% Overflow
 1.15942% Exp_not_supported:UnOpLNot
 0.73399% Bitwisebinop
 0.38803% Exp_not_supported:LValVar.Index
 0.35998% (Cast_not_injectiveunsigned
... <1% other

The other data does not immediately suggest any other changes imho, so I would consider this the only change for now.